The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

0 CpxRelTRS
↳1 RenamingProof (⇔, 0 ms)
↳2 CpxRelTRS
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 13 ms)
↳4 typed CpxTrs
↳5 OrderProof (LOWER BOUND(ID), 0 ms)
↳6 typed CpxTrs
↳7 RewriteLemmaProof (LOWER BOUND(ID), 375 ms)
↳8 BEST
    ↳9 typed CpxTrs
        ↳10 RewriteLemmaProof (LOWER BOUND(ID), 33 ms)
        ↳11 BEST
            ↳12 typed CpxTrs
                ↳13 NoRewriteLemmaProof (LOWER BOUND(ID), 21 ms)
                ↳14 typed CpxTrs
                ↳15 LowerBoundsProof (⇔, 0 ms)
                ↳16 BOUNDS(n^1, INF)
            ↳17 typed CpxTrs
                ↳18 LowerBoundsProof (⇔, 0 ms)
                ↳19 BOUNDS(n^1, INF)
    ↳20 typed CpxTrs
        ↳21 LowerBoundsProof (⇔, 0 ms)
        ↳22 BOUNDS(1, INF)

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

turing(I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog) → turing[Ite](!EQ(x, i1), I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog)
turing(I(Goto(int), r), revltape, rtape, prog) → turing(lookup(int, prog), revltape, rtape, prog)
turing(I(Right, r), revltape, Cons(x, xs), prog) → turing(r, Cons(x, revltape), xs, prog)
turing(I(Right, r), revltape, Nil, prog) → turing(r, Cons(0, revltape), Nil, prog)
turing(I(Left, r), Cons(x, xs), rtape, prog) → turing(r, xs, Cons(x, rtape), prog)
turing(I(Left, r), Nil, rtape, prog) → turing(r, Nil, Cons(0, rtape), prog)
turing(I(Write(int), r), revltape, Cons(x, xs), prog) → turing(r, revltape, Cons(int, xs), prog)
turing(I(Halt, r), revltape, rtape, prog) → rtape
turing(Empty, revltape, rtape, prog) → rtape
lookup(S(x), I(l, r)) → lookup(x, r)
instrsConstrCheck(I(l1, r1), I(x, y)) → True
instrsConstrCheck(I(l1, r1), Empty) → False
instrsConstrCheck(Empty, I(x, y)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), IfGoto(igtNat12, igtNat22)) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Right) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Left) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt) → False
instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Goto(gtNat), Goto(gtNat2)) → True
instrConstrCheck(Goto(gtNat), Right) → False
instrConstrCheck(Goto(gtNat), Left) → False
instrConstrCheck(Goto(gtNat), Write(wNat2)) → False
instrConstrCheck(Goto(gtNat), Halt) → False
instrConstrCheck(Right, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Right, Goto(gtNat2)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(wNat2)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Left, Goto(gtNat2)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(wNat2)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Write(wNat), Goto(gtNat2)) → False
instrConstrCheck(Write(wNat), Right) → False
instrConstrCheck(Write(wNat), Left) → False
instrConstrCheck(Write(wNat), Write(wNat2)) → True
instrConstrCheck(Write(wNat), Halt) → False
instrConstrCheck(Halt, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Halt, Goto(gtNat2)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(wNat2)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lookup(0, instrs) → instrs
instrsSecond(I(l, r)) → r
instrsFirst(I(l, r)) → l
getWrite(Write(int)) → int
getGotoSecond(IfGoto(i1, i2)) → i2
getGotoFirst(IfGoto(i1, i2)) → i1
getGoto(Goto(int)) → int
run(prog, tapeinput) → turing(prog, Nil, tapeinput, prog)

The (relative) TRS S consists of the following rules:

!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
turing[Ite](True, I(IfGoto(i1, i2), r), revltape, rtape, prog) → turing(lookup(i2, prog), revltape, rtape, prog)
turing[Ite](False, I(l, r), revltape, rtape, prog) → turing(r, revltape, rtape, prog)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

turing(I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog) → turing[Ite](!EQ(x, i1), I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog)
turing(I(Goto(int), r), revltape, rtape, prog) → turing(lookup(int, prog), revltape, rtape, prog)
turing(I(Right, r), revltape, Cons(x, xs), prog) → turing(r, Cons(x, revltape), xs, prog)
turing(I(Right, r), revltape, Nil, prog) → turing(r, Cons(0', revltape), Nil, prog)
turing(I(Left, r), Cons(x, xs), rtape, prog) → turing(r, xs, Cons(x, rtape), prog)
turing(I(Left, r), Nil, rtape, prog) → turing(r, Nil, Cons(0', rtape), prog)
turing(I(Write(int), r), revltape, Cons(x, xs), prog) → turing(r, revltape, Cons(int, xs), prog)
turing(I(Halt, r), revltape, rtape, prog) → rtape
turing(Empty, revltape, rtape, prog) → rtape
lookup(S(x), I(l, r)) → lookup(x, r)
instrsConstrCheck(I(l1, r1), I(x, y)) → True
instrsConstrCheck(I(l1, r1), Empty) → False
instrsConstrCheck(Empty, I(x, y)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), IfGoto(igtNat12, igtNat22)) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Right) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Left) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt) → False
instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Goto(gtNat), Goto(gtNat2)) → True
instrConstrCheck(Goto(gtNat), Right) → False
instrConstrCheck(Goto(gtNat), Left) → False
instrConstrCheck(Goto(gtNat), Write(wNat2)) → False
instrConstrCheck(Goto(gtNat), Halt) → False
instrConstrCheck(Right, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Right, Goto(gtNat2)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(wNat2)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Left, Goto(gtNat2)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(wNat2)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Write(wNat), Goto(gtNat2)) → False
instrConstrCheck(Write(wNat), Right) → False
instrConstrCheck(Write(wNat), Left) → False
instrConstrCheck(Write(wNat), Write(wNat2)) → True
instrConstrCheck(Write(wNat), Halt) → False
instrConstrCheck(Halt, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Halt, Goto(gtNat2)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(wNat2)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lookup(0', instrs) → instrs
instrsSecond(I(l, r)) → r
instrsFirst(I(l, r)) → l
getWrite(Write(int)) → int
getGotoSecond(IfGoto(i1, i2)) → i2
getGotoFirst(IfGoto(i1, i2)) → i1
getGoto(Goto(int)) → int
run(prog, tapeinput) → turing(prog, Nil, tapeinput, prog)

The (relative) TRS S consists of the following rules:

!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
turing[Ite](True, I(IfGoto(i1, i2), r), revltape, rtape, prog) → turing(lookup(i2, prog), revltape, rtape, prog)
turing[Ite](False, I(l, r), revltape, rtape, prog) → turing(r, revltape, rtape, prog)

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
turing(I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog) → turing[Ite](!EQ(x, i1), I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog)
turing(I(Goto(int), r), revltape, rtape, prog) → turing(lookup(int, prog), revltape, rtape, prog)
turing(I(Right, r), revltape, Cons(x, xs), prog) → turing(r, Cons(x, revltape), xs, prog)
turing(I(Right, r), revltape, Nil, prog) → turing(r, Cons(0', revltape), Nil, prog)
turing(I(Left, r), Cons(x, xs), rtape, prog) → turing(r, xs, Cons(x, rtape), prog)
turing(I(Left, r), Nil, rtape, prog) → turing(r, Nil, Cons(0', rtape), prog)
turing(I(Write(int), r), revltape, Cons(x, xs), prog) → turing(r, revltape, Cons(int, xs), prog)
turing(I(Halt, r), revltape, rtape, prog) → rtape
turing(Empty, revltape, rtape, prog) → rtape
lookup(S(x), I(l, r)) → lookup(x, r)
instrsConstrCheck(I(l1, r1), I(x, y)) → True
instrsConstrCheck(I(l1, r1), Empty) → False
instrsConstrCheck(Empty, I(x, y)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), IfGoto(igtNat12, igtNat22)) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Right) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Left) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt) → False
instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Goto(gtNat), Goto(gtNat2)) → True
instrConstrCheck(Goto(gtNat), Right) → False
instrConstrCheck(Goto(gtNat), Left) → False
instrConstrCheck(Goto(gtNat), Write(wNat2)) → False
instrConstrCheck(Goto(gtNat), Halt) → False
instrConstrCheck(Right, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Right, Goto(gtNat2)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(wNat2)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Left, Goto(gtNat2)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(wNat2)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Write(wNat), Goto(gtNat2)) → False
instrConstrCheck(Write(wNat), Right) → False
instrConstrCheck(Write(wNat), Left) → False
instrConstrCheck(Write(wNat), Write(wNat2)) → True
instrConstrCheck(Write(wNat), Halt) → False
instrConstrCheck(Halt, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Halt, Goto(gtNat2)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(wNat2)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lookup(0', instrs) → instrs
instrsSecond(I(l, r)) → r
instrsFirst(I(l, r)) → l
getWrite(Write(int)) → int
getGotoSecond(IfGoto(i1, i2)) → i2
getGotoFirst(IfGoto(i1, i2)) → i1
getGoto(Goto(int)) → int
run(prog, tapeinput) → turing(prog, Nil, tapeinput, prog)
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
turing[Ite](True, I(IfGoto(i1, i2), r), revltape, rtape, prog) → turing(lookup(i2, prog), revltape, rtape, prog)
turing[Ite](False, I(l, r), revltape, rtape, prog) → turing(r, revltape, rtape, prog)

Types:
turing :: I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
I :: IfGoto:Goto:Right:Left:Write:Halt → I:Empty → I:Empty
IfGoto :: 0':S → 0':S → IfGoto:Goto:Right:Left:Write:Halt
Cons :: 0':S → Cons:Nil → Cons:Nil
turing[Ite] :: True:False → I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
!EQ :: 0':S → 0':S → True:False
Goto :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
lookup :: 0':S → I:Empty → I:Empty
Right :: IfGoto:Goto:Right:Left:Write:Halt
Nil :: Cons:Nil
0' :: 0':S
Left :: IfGoto:Goto:Right:Left:Write:Halt
Write :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
Halt :: IfGoto:Goto:Right:Left:Write:Halt
Empty :: I:Empty
S :: 0':S → 0':S
instrsConstrCheck :: I:Empty → I:Empty → True:False
True :: True:False
False :: True:False
instrConstrCheck :: IfGoto:Goto:Right:Left:Write:Halt → IfGoto:Goto:Right:Left:Write:Halt → True:False
notEmpty :: Cons:Nil → True:False
instrsSecond :: I:Empty → I:Empty
instrsFirst :: I:Empty → IfGoto:Goto:Right:Left:Write:Halt
getWrite :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoSecond :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoFirst :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGoto :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
run :: I:Empty → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_I:Empty2_0 :: I:Empty
hole_IfGoto:Goto:Right:Left:Write:Halt3_0 :: IfGoto:Goto:Right:Left:Write:Halt
hole_0':S4_0 :: 0':S
hole_True:False5_0 :: True:False
gen_Cons:Nil6_0 :: Nat → Cons:Nil
gen_I:Empty7_0 :: Nat → I:Empty
gen_0':S8_0 :: Nat → 0':S

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
turing, !EQ, lookup

They will be analysed ascendingly in the following order:
!EQ < turing
lookup < turing

(6) Obligation:

Innermost TRS:
Rules:
turing(I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog) → turing[Ite](!EQ(x, i1), I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog)
turing(I(Goto(int), r), revltape, rtape, prog) → turing(lookup(int, prog), revltape, rtape, prog)
turing(I(Right, r), revltape, Cons(x, xs), prog) → turing(r, Cons(x, revltape), xs, prog)
turing(I(Right, r), revltape, Nil, prog) → turing(r, Cons(0', revltape), Nil, prog)
turing(I(Left, r), Cons(x, xs), rtape, prog) → turing(r, xs, Cons(x, rtape), prog)
turing(I(Left, r), Nil, rtape, prog) → turing(r, Nil, Cons(0', rtape), prog)
turing(I(Write(int), r), revltape, Cons(x, xs), prog) → turing(r, revltape, Cons(int, xs), prog)
turing(I(Halt, r), revltape, rtape, prog) → rtape
turing(Empty, revltape, rtape, prog) → rtape
lookup(S(x), I(l, r)) → lookup(x, r)
instrsConstrCheck(I(l1, r1), I(x, y)) → True
instrsConstrCheck(I(l1, r1), Empty) → False
instrsConstrCheck(Empty, I(x, y)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), IfGoto(igtNat12, igtNat22)) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Right) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Left) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt) → False
instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Goto(gtNat), Goto(gtNat2)) → True
instrConstrCheck(Goto(gtNat), Right) → False
instrConstrCheck(Goto(gtNat), Left) → False
instrConstrCheck(Goto(gtNat), Write(wNat2)) → False
instrConstrCheck(Goto(gtNat), Halt) → False
instrConstrCheck(Right, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Right, Goto(gtNat2)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(wNat2)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Left, Goto(gtNat2)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(wNat2)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Write(wNat), Goto(gtNat2)) → False
instrConstrCheck(Write(wNat), Right) → False
instrConstrCheck(Write(wNat), Left) → False
instrConstrCheck(Write(wNat), Write(wNat2)) → True
instrConstrCheck(Write(wNat), Halt) → False
instrConstrCheck(Halt, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Halt, Goto(gtNat2)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(wNat2)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lookup(0', instrs) → instrs
instrsSecond(I(l, r)) → r
instrsFirst(I(l, r)) → l
getWrite(Write(int)) → int
getGotoSecond(IfGoto(i1, i2)) → i2
getGotoFirst(IfGoto(i1, i2)) → i1
getGoto(Goto(int)) → int
run(prog, tapeinput) → turing(prog, Nil, tapeinput, prog)
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
turing[Ite](True, I(IfGoto(i1, i2), r), revltape, rtape, prog) → turing(lookup(i2, prog), revltape, rtape, prog)
turing[Ite](False, I(l, r), revltape, rtape, prog) → turing(r, revltape, rtape, prog)

Types:
turing :: I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
I :: IfGoto:Goto:Right:Left:Write:Halt → I:Empty → I:Empty
IfGoto :: 0':S → 0':S → IfGoto:Goto:Right:Left:Write:Halt
Cons :: 0':S → Cons:Nil → Cons:Nil
turing[Ite] :: True:False → I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
!EQ :: 0':S → 0':S → True:False
Goto :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
lookup :: 0':S → I:Empty → I:Empty
Right :: IfGoto:Goto:Right:Left:Write:Halt
Nil :: Cons:Nil
0' :: 0':S
Left :: IfGoto:Goto:Right:Left:Write:Halt
Write :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
Halt :: IfGoto:Goto:Right:Left:Write:Halt
Empty :: I:Empty
S :: 0':S → 0':S
instrsConstrCheck :: I:Empty → I:Empty → True:False
True :: True:False
False :: True:False
instrConstrCheck :: IfGoto:Goto:Right:Left:Write:Halt → IfGoto:Goto:Right:Left:Write:Halt → True:False
notEmpty :: Cons:Nil → True:False
instrsSecond :: I:Empty → I:Empty
instrsFirst :: I:Empty → IfGoto:Goto:Right:Left:Write:Halt
getWrite :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoSecond :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoFirst :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGoto :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
run :: I:Empty → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_I:Empty2_0 :: I:Empty
hole_IfGoto:Goto:Right:Left:Write:Halt3_0 :: IfGoto:Goto:Right:Left:Write:Halt
hole_0':S4_0 :: 0':S
hole_True:False5_0 :: True:False
gen_Cons:Nil6_0 :: Nat → Cons:Nil
gen_I:Empty7_0 :: Nat → I:Empty
gen_0':S8_0 :: Nat → 0':S

Generator Equations:
gen_Cons:Nil6_0(0) ⇔ Nil
gen_Cons:Nil6_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil6_0(x))
gen_I:Empty7_0(0) ⇔ Empty
gen_I:Empty7_0(+(x, 1)) ⇔ I(IfGoto(0', 0'), gen_I:Empty7_0(x))
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))

The following defined symbols remain to be analysed:
!EQ, turing, lookup

They will be analysed ascendingly in the following order:
!EQ < turing
lookup < turing

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
!EQ(gen_0':S8_0(n10_0), gen_0':S8_0(+(1, n10_0))) → False, rt ∈ Ω(0)

Induction Base:
!EQ(gen_0':S8_0(0), gen_0':S8_0(+(1, 0))) →RΩ(0)
False

Induction Step:
!EQ(gen_0':S8_0(+(n10_0, 1)), gen_0':S8_0(+(1, +(n10_0, 1)))) →RΩ(0)
!EQ(gen_0':S8_0(n10_0), gen_0':S8_0(+(1, n10_0))) →IH
False

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
turing(I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog) → turing[Ite](!EQ(x, i1), I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog)
turing(I(Goto(int), r), revltape, rtape, prog) → turing(lookup(int, prog), revltape, rtape, prog)
turing(I(Right, r), revltape, Cons(x, xs), prog) → turing(r, Cons(x, revltape), xs, prog)
turing(I(Right, r), revltape, Nil, prog) → turing(r, Cons(0', revltape), Nil, prog)
turing(I(Left, r), Cons(x, xs), rtape, prog) → turing(r, xs, Cons(x, rtape), prog)
turing(I(Left, r), Nil, rtape, prog) → turing(r, Nil, Cons(0', rtape), prog)
turing(I(Write(int), r), revltape, Cons(x, xs), prog) → turing(r, revltape, Cons(int, xs), prog)
turing(I(Halt, r), revltape, rtape, prog) → rtape
turing(Empty, revltape, rtape, prog) → rtape
lookup(S(x), I(l, r)) → lookup(x, r)
instrsConstrCheck(I(l1, r1), I(x, y)) → True
instrsConstrCheck(I(l1, r1), Empty) → False
instrsConstrCheck(Empty, I(x, y)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), IfGoto(igtNat12, igtNat22)) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Right) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Left) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt) → False
instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Goto(gtNat), Goto(gtNat2)) → True
instrConstrCheck(Goto(gtNat), Right) → False
instrConstrCheck(Goto(gtNat), Left) → False
instrConstrCheck(Goto(gtNat), Write(wNat2)) → False
instrConstrCheck(Goto(gtNat), Halt) → False
instrConstrCheck(Right, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Right, Goto(gtNat2)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(wNat2)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Left, Goto(gtNat2)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(wNat2)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Write(wNat), Goto(gtNat2)) → False
instrConstrCheck(Write(wNat), Right) → False
instrConstrCheck(Write(wNat), Left) → False
instrConstrCheck(Write(wNat), Write(wNat2)) → True
instrConstrCheck(Write(wNat), Halt) → False
instrConstrCheck(Halt, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Halt, Goto(gtNat2)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(wNat2)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lookup(0', instrs) → instrs
instrsSecond(I(l, r)) → r
instrsFirst(I(l, r)) → l
getWrite(Write(int)) → int
getGotoSecond(IfGoto(i1, i2)) → i2
getGotoFirst(IfGoto(i1, i2)) → i1
getGoto(Goto(int)) → int
run(prog, tapeinput) → turing(prog, Nil, tapeinput, prog)
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
turing[Ite](True, I(IfGoto(i1, i2), r), revltape, rtape, prog) → turing(lookup(i2, prog), revltape, rtape, prog)
turing[Ite](False, I(l, r), revltape, rtape, prog) → turing(r, revltape, rtape, prog)

Types:
turing :: I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
I :: IfGoto:Goto:Right:Left:Write:Halt → I:Empty → I:Empty
IfGoto :: 0':S → 0':S → IfGoto:Goto:Right:Left:Write:Halt
Cons :: 0':S → Cons:Nil → Cons:Nil
turing[Ite] :: True:False → I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
!EQ :: 0':S → 0':S → True:False
Goto :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
lookup :: 0':S → I:Empty → I:Empty
Right :: IfGoto:Goto:Right:Left:Write:Halt
Nil :: Cons:Nil
0' :: 0':S
Left :: IfGoto:Goto:Right:Left:Write:Halt
Write :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
Halt :: IfGoto:Goto:Right:Left:Write:Halt
Empty :: I:Empty
S :: 0':S → 0':S
instrsConstrCheck :: I:Empty → I:Empty → True:False
True :: True:False
False :: True:False
instrConstrCheck :: IfGoto:Goto:Right:Left:Write:Halt → IfGoto:Goto:Right:Left:Write:Halt → True:False
notEmpty :: Cons:Nil → True:False
instrsSecond :: I:Empty → I:Empty
instrsFirst :: I:Empty → IfGoto:Goto:Right:Left:Write:Halt
getWrite :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoSecond :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoFirst :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGoto :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
run :: I:Empty → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_I:Empty2_0 :: I:Empty
hole_IfGoto:Goto:Right:Left:Write:Halt3_0 :: IfGoto:Goto:Right:Left:Write:Halt
hole_0':S4_0 :: 0':S
hole_True:False5_0 :: True:False
gen_Cons:Nil6_0 :: Nat → Cons:Nil
gen_I:Empty7_0 :: Nat → I:Empty
gen_0':S8_0 :: Nat → 0':S

Lemmas:
!EQ(gen_0':S8_0(n10_0), gen_0':S8_0(+(1, n10_0))) → False, rt ∈ Ω(0)

Generator Equations:
gen_Cons:Nil6_0(0) ⇔ Nil
gen_Cons:Nil6_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil6_0(x))
gen_I:Empty7_0(0) ⇔ Empty
gen_I:Empty7_0(+(x, 1)) ⇔ I(IfGoto(0', 0'), gen_I:Empty7_0(x))
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))

The following defined symbols remain to be analysed:
lookup, turing

They will be analysed ascendingly in the following order:
lookup < turing

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
lookup(gen_0':S8_0(n673_0), gen_I:Empty7_0(n673_0)) → gen_I:Empty7_0(0), rt ∈ Ω(1 + n6730)

Induction Base:
lookup(gen_0':S8_0(0), gen_I:Empty7_0(0)) →RΩ(1)
gen_I:Empty7_0(0)

Induction Step:
lookup(gen_0':S8_0(+(n673_0, 1)), gen_I:Empty7_0(+(n673_0, 1))) →RΩ(1)
lookup(gen_0':S8_0(n673_0), gen_I:Empty7_0(n673_0)) →IH
gen_I:Empty7_0(0)

We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

(11) Complex Obligation (BEST)

(12) Obligation:

Innermost TRS:
Rules:
turing(I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog) → turing[Ite](!EQ(x, i1), I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog)
turing(I(Goto(int), r), revltape, rtape, prog) → turing(lookup(int, prog), revltape, rtape, prog)
turing(I(Right, r), revltape, Cons(x, xs), prog) → turing(r, Cons(x, revltape), xs, prog)
turing(I(Right, r), revltape, Nil, prog) → turing(r, Cons(0', revltape), Nil, prog)
turing(I(Left, r), Cons(x, xs), rtape, prog) → turing(r, xs, Cons(x, rtape), prog)
turing(I(Left, r), Nil, rtape, prog) → turing(r, Nil, Cons(0', rtape), prog)
turing(I(Write(int), r), revltape, Cons(x, xs), prog) → turing(r, revltape, Cons(int, xs), prog)
turing(I(Halt, r), revltape, rtape, prog) → rtape
turing(Empty, revltape, rtape, prog) → rtape
lookup(S(x), I(l, r)) → lookup(x, r)
instrsConstrCheck(I(l1, r1), I(x, y)) → True
instrsConstrCheck(I(l1, r1), Empty) → False
instrsConstrCheck(Empty, I(x, y)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), IfGoto(igtNat12, igtNat22)) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Right) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Left) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt) → False
instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Goto(gtNat), Goto(gtNat2)) → True
instrConstrCheck(Goto(gtNat), Right) → False
instrConstrCheck(Goto(gtNat), Left) → False
instrConstrCheck(Goto(gtNat), Write(wNat2)) → False
instrConstrCheck(Goto(gtNat), Halt) → False
instrConstrCheck(Right, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Right, Goto(gtNat2)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(wNat2)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Left, Goto(gtNat2)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(wNat2)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Write(wNat), Goto(gtNat2)) → False
instrConstrCheck(Write(wNat), Right) → False
instrConstrCheck(Write(wNat), Left) → False
instrConstrCheck(Write(wNat), Write(wNat2)) → True
instrConstrCheck(Write(wNat), Halt) → False
instrConstrCheck(Halt, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Halt, Goto(gtNat2)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(wNat2)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lookup(0', instrs) → instrs
instrsSecond(I(l, r)) → r
instrsFirst(I(l, r)) → l
getWrite(Write(int)) → int
getGotoSecond(IfGoto(i1, i2)) → i2
getGotoFirst(IfGoto(i1, i2)) → i1
getGoto(Goto(int)) → int
run(prog, tapeinput) → turing(prog, Nil, tapeinput, prog)
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
turing[Ite](True, I(IfGoto(i1, i2), r), revltape, rtape, prog) → turing(lookup(i2, prog), revltape, rtape, prog)
turing[Ite](False, I(l, r), revltape, rtape, prog) → turing(r, revltape, rtape, prog)

Types:
turing :: I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
I :: IfGoto:Goto:Right:Left:Write:Halt → I:Empty → I:Empty
IfGoto :: 0':S → 0':S → IfGoto:Goto:Right:Left:Write:Halt
Cons :: 0':S → Cons:Nil → Cons:Nil
turing[Ite] :: True:False → I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
!EQ :: 0':S → 0':S → True:False
Goto :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
lookup :: 0':S → I:Empty → I:Empty
Right :: IfGoto:Goto:Right:Left:Write:Halt
Nil :: Cons:Nil
0' :: 0':S
Left :: IfGoto:Goto:Right:Left:Write:Halt
Write :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
Halt :: IfGoto:Goto:Right:Left:Write:Halt
Empty :: I:Empty
S :: 0':S → 0':S
instrsConstrCheck :: I:Empty → I:Empty → True:False
True :: True:False
False :: True:False
instrConstrCheck :: IfGoto:Goto:Right:Left:Write:Halt → IfGoto:Goto:Right:Left:Write:Halt → True:False
notEmpty :: Cons:Nil → True:False
instrsSecond :: I:Empty → I:Empty
instrsFirst :: I:Empty → IfGoto:Goto:Right:Left:Write:Halt
getWrite :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoSecond :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoFirst :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGoto :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
run :: I:Empty → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_I:Empty2_0 :: I:Empty
hole_IfGoto:Goto:Right:Left:Write:Halt3_0 :: IfGoto:Goto:Right:Left:Write:Halt
hole_0':S4_0 :: 0':S
hole_True:False5_0 :: True:False
gen_Cons:Nil6_0 :: Nat → Cons:Nil
gen_I:Empty7_0 :: Nat → I:Empty
gen_0':S8_0 :: Nat → 0':S

Lemmas:
!EQ(gen_0':S8_0(n10_0), gen_0':S8_0(+(1, n10_0))) → False, rt ∈ Ω(0)
lookup(gen_0':S8_0(n673_0), gen_I:Empty7_0(n673_0)) → gen_I:Empty7_0(0), rt ∈ Ω(1 + n6730)

Generator Equations:
gen_Cons:Nil6_0(0) ⇔ Nil
gen_Cons:Nil6_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil6_0(x))
gen_I:Empty7_0(0) ⇔ Empty
gen_I:Empty7_0(+(x, 1)) ⇔ I(IfGoto(0', 0'), gen_I:Empty7_0(x))
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))

The following defined symbols remain to be analysed:
turing

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol turing.

(14) Obligation:

Innermost TRS:
Rules:
turing(I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog) → turing[Ite](!EQ(x, i1), I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog)
turing(I(Goto(int), r), revltape, rtape, prog) → turing(lookup(int, prog), revltape, rtape, prog)
turing(I(Right, r), revltape, Cons(x, xs), prog) → turing(r, Cons(x, revltape), xs, prog)
turing(I(Right, r), revltape, Nil, prog) → turing(r, Cons(0', revltape), Nil, prog)
turing(I(Left, r), Cons(x, xs), rtape, prog) → turing(r, xs, Cons(x, rtape), prog)
turing(I(Left, r), Nil, rtape, prog) → turing(r, Nil, Cons(0', rtape), prog)
turing(I(Write(int), r), revltape, Cons(x, xs), prog) → turing(r, revltape, Cons(int, xs), prog)
turing(I(Halt, r), revltape, rtape, prog) → rtape
turing(Empty, revltape, rtape, prog) → rtape
lookup(S(x), I(l, r)) → lookup(x, r)
instrsConstrCheck(I(l1, r1), I(x, y)) → True
instrsConstrCheck(I(l1, r1), Empty) → False
instrsConstrCheck(Empty, I(x, y)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), IfGoto(igtNat12, igtNat22)) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Right) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Left) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt) → False
instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Goto(gtNat), Goto(gtNat2)) → True
instrConstrCheck(Goto(gtNat), Right) → False
instrConstrCheck(Goto(gtNat), Left) → False
instrConstrCheck(Goto(gtNat), Write(wNat2)) → False
instrConstrCheck(Goto(gtNat), Halt) → False
instrConstrCheck(Right, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Right, Goto(gtNat2)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(wNat2)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Left, Goto(gtNat2)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(wNat2)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Write(wNat), Goto(gtNat2)) → False
instrConstrCheck(Write(wNat), Right) → False
instrConstrCheck(Write(wNat), Left) → False
instrConstrCheck(Write(wNat), Write(wNat2)) → True
instrConstrCheck(Write(wNat), Halt) → False
instrConstrCheck(Halt, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Halt, Goto(gtNat2)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(wNat2)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lookup(0', instrs) → instrs
instrsSecond(I(l, r)) → r
instrsFirst(I(l, r)) → l
getWrite(Write(int)) → int
getGotoSecond(IfGoto(i1, i2)) → i2
getGotoFirst(IfGoto(i1, i2)) → i1
getGoto(Goto(int)) → int
run(prog, tapeinput) → turing(prog, Nil, tapeinput, prog)
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
turing[Ite](True, I(IfGoto(i1, i2), r), revltape, rtape, prog) → turing(lookup(i2, prog), revltape, rtape, prog)
turing[Ite](False, I(l, r), revltape, rtape, prog) → turing(r, revltape, rtape, prog)

Types:
turing :: I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
I :: IfGoto:Goto:Right:Left:Write:Halt → I:Empty → I:Empty
IfGoto :: 0':S → 0':S → IfGoto:Goto:Right:Left:Write:Halt
Cons :: 0':S → Cons:Nil → Cons:Nil
turing[Ite] :: True:False → I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
!EQ :: 0':S → 0':S → True:False
Goto :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
lookup :: 0':S → I:Empty → I:Empty
Right :: IfGoto:Goto:Right:Left:Write:Halt
Nil :: Cons:Nil
0' :: 0':S
Left :: IfGoto:Goto:Right:Left:Write:Halt
Write :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
Halt :: IfGoto:Goto:Right:Left:Write:Halt
Empty :: I:Empty
S :: 0':S → 0':S
instrsConstrCheck :: I:Empty → I:Empty → True:False
True :: True:False
False :: True:False
instrConstrCheck :: IfGoto:Goto:Right:Left:Write:Halt → IfGoto:Goto:Right:Left:Write:Halt → True:False
notEmpty :: Cons:Nil → True:False
instrsSecond :: I:Empty → I:Empty
instrsFirst :: I:Empty → IfGoto:Goto:Right:Left:Write:Halt
getWrite :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoSecond :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoFirst :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGoto :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
run :: I:Empty → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_I:Empty2_0 :: I:Empty
hole_IfGoto:Goto:Right:Left:Write:Halt3_0 :: IfGoto:Goto:Right:Left:Write:Halt
hole_0':S4_0 :: 0':S
hole_True:False5_0 :: True:False
gen_Cons:Nil6_0 :: Nat → Cons:Nil
gen_I:Empty7_0 :: Nat → I:Empty
gen_0':S8_0 :: Nat → 0':S

Lemmas:
!EQ(gen_0':S8_0(n10_0), gen_0':S8_0(+(1, n10_0))) → False, rt ∈ Ω(0)
lookup(gen_0':S8_0(n673_0), gen_I:Empty7_0(n673_0)) → gen_I:Empty7_0(0), rt ∈ Ω(1 + n6730)

Generator Equations:
gen_Cons:Nil6_0(0) ⇔ Nil
gen_Cons:Nil6_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil6_0(x))
gen_I:Empty7_0(0) ⇔ Empty
gen_I:Empty7_0(+(x, 1)) ⇔ I(IfGoto(0', 0'), gen_I:Empty7_0(x))
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))

No more defined symbols left to analyse.

(15) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
lookup(gen_0':S8_0(n673_0), gen_I:Empty7_0(n673_0)) → gen_I:Empty7_0(0), rt ∈ Ω(1 + n6730)

(16) BOUNDS(n^1, INF)

(17) Obligation:

Innermost TRS:
Rules:
turing(I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog) → turing[Ite](!EQ(x, i1), I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog)
turing(I(Goto(int), r), revltape, rtape, prog) → turing(lookup(int, prog), revltape, rtape, prog)
turing(I(Right, r), revltape, Cons(x, xs), prog) → turing(r, Cons(x, revltape), xs, prog)
turing(I(Right, r), revltape, Nil, prog) → turing(r, Cons(0', revltape), Nil, prog)
turing(I(Left, r), Cons(x, xs), rtape, prog) → turing(r, xs, Cons(x, rtape), prog)
turing(I(Left, r), Nil, rtape, prog) → turing(r, Nil, Cons(0', rtape), prog)
turing(I(Write(int), r), revltape, Cons(x, xs), prog) → turing(r, revltape, Cons(int, xs), prog)
turing(I(Halt, r), revltape, rtape, prog) → rtape
turing(Empty, revltape, rtape, prog) → rtape
lookup(S(x), I(l, r)) → lookup(x, r)
instrsConstrCheck(I(l1, r1), I(x, y)) → True
instrsConstrCheck(I(l1, r1), Empty) → False
instrsConstrCheck(Empty, I(x, y)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), IfGoto(igtNat12, igtNat22)) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Right) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Left) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt) → False
instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Goto(gtNat), Goto(gtNat2)) → True
instrConstrCheck(Goto(gtNat), Right) → False
instrConstrCheck(Goto(gtNat), Left) → False
instrConstrCheck(Goto(gtNat), Write(wNat2)) → False
instrConstrCheck(Goto(gtNat), Halt) → False
instrConstrCheck(Right, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Right, Goto(gtNat2)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(wNat2)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Left, Goto(gtNat2)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(wNat2)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Write(wNat), Goto(gtNat2)) → False
instrConstrCheck(Write(wNat), Right) → False
instrConstrCheck(Write(wNat), Left) → False
instrConstrCheck(Write(wNat), Write(wNat2)) → True
instrConstrCheck(Write(wNat), Halt) → False
instrConstrCheck(Halt, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Halt, Goto(gtNat2)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(wNat2)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lookup(0', instrs) → instrs
instrsSecond(I(l, r)) → r
instrsFirst(I(l, r)) → l
getWrite(Write(int)) → int
getGotoSecond(IfGoto(i1, i2)) → i2
getGotoFirst(IfGoto(i1, i2)) → i1
getGoto(Goto(int)) → int
run(prog, tapeinput) → turing(prog, Nil, tapeinput, prog)
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
turing[Ite](True, I(IfGoto(i1, i2), r), revltape, rtape, prog) → turing(lookup(i2, prog), revltape, rtape, prog)
turing[Ite](False, I(l, r), revltape, rtape, prog) → turing(r, revltape, rtape, prog)

Types:
turing :: I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
I :: IfGoto:Goto:Right:Left:Write:Halt → I:Empty → I:Empty
IfGoto :: 0':S → 0':S → IfGoto:Goto:Right:Left:Write:Halt
Cons :: 0':S → Cons:Nil → Cons:Nil
turing[Ite] :: True:False → I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
!EQ :: 0':S → 0':S → True:False
Goto :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
lookup :: 0':S → I:Empty → I:Empty
Right :: IfGoto:Goto:Right:Left:Write:Halt
Nil :: Cons:Nil
0' :: 0':S
Left :: IfGoto:Goto:Right:Left:Write:Halt
Write :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
Halt :: IfGoto:Goto:Right:Left:Write:Halt
Empty :: I:Empty
S :: 0':S → 0':S
instrsConstrCheck :: I:Empty → I:Empty → True:False
True :: True:False
False :: True:False
instrConstrCheck :: IfGoto:Goto:Right:Left:Write:Halt → IfGoto:Goto:Right:Left:Write:Halt → True:False
notEmpty :: Cons:Nil → True:False
instrsSecond :: I:Empty → I:Empty
instrsFirst :: I:Empty → IfGoto:Goto:Right:Left:Write:Halt
getWrite :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoSecond :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoFirst :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGoto :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
run :: I:Empty → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_I:Empty2_0 :: I:Empty
hole_IfGoto:Goto:Right:Left:Write:Halt3_0 :: IfGoto:Goto:Right:Left:Write:Halt
hole_0':S4_0 :: 0':S
hole_True:False5_0 :: True:False
gen_Cons:Nil6_0 :: Nat → Cons:Nil
gen_I:Empty7_0 :: Nat → I:Empty
gen_0':S8_0 :: Nat → 0':S

Lemmas:
!EQ(gen_0':S8_0(n10_0), gen_0':S8_0(+(1, n10_0))) → False, rt ∈ Ω(0)
lookup(gen_0':S8_0(n673_0), gen_I:Empty7_0(n673_0)) → gen_I:Empty7_0(0), rt ∈ Ω(1 + n6730)

Generator Equations:
gen_Cons:Nil6_0(0) ⇔ Nil
gen_Cons:Nil6_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil6_0(x))
gen_I:Empty7_0(0) ⇔ Empty
gen_I:Empty7_0(+(x, 1)) ⇔ I(IfGoto(0', 0'), gen_I:Empty7_0(x))
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))

No more defined symbols left to analyse.

(18) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
lookup(gen_0':S8_0(n673_0), gen_I:Empty7_0(n673_0)) → gen_I:Empty7_0(0), rt ∈ Ω(1 + n6730)

(19) BOUNDS(n^1, INF)

(20) Obligation:

Innermost TRS:
Rules:
turing(I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog) → turing[Ite](!EQ(x, i1), I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog)
turing(I(Goto(int), r), revltape, rtape, prog) → turing(lookup(int, prog), revltape, rtape, prog)
turing(I(Right, r), revltape, Cons(x, xs), prog) → turing(r, Cons(x, revltape), xs, prog)
turing(I(Right, r), revltape, Nil, prog) → turing(r, Cons(0', revltape), Nil, prog)
turing(I(Left, r), Cons(x, xs), rtape, prog) → turing(r, xs, Cons(x, rtape), prog)
turing(I(Left, r), Nil, rtape, prog) → turing(r, Nil, Cons(0', rtape), prog)
turing(I(Write(int), r), revltape, Cons(x, xs), prog) → turing(r, revltape, Cons(int, xs), prog)
turing(I(Halt, r), revltape, rtape, prog) → rtape
turing(Empty, revltape, rtape, prog) → rtape
lookup(S(x), I(l, r)) → lookup(x, r)
instrsConstrCheck(I(l1, r1), I(x, y)) → True
instrsConstrCheck(I(l1, r1), Empty) → False
instrsConstrCheck(Empty, I(x, y)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), IfGoto(igtNat12, igtNat22)) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Right) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Left) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt) → False
instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Goto(gtNat), Goto(gtNat2)) → True
instrConstrCheck(Goto(gtNat), Right) → False
instrConstrCheck(Goto(gtNat), Left) → False
instrConstrCheck(Goto(gtNat), Write(wNat2)) → False
instrConstrCheck(Goto(gtNat), Halt) → False
instrConstrCheck(Right, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Right, Goto(gtNat2)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(wNat2)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Left, Goto(gtNat2)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(wNat2)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Write(wNat), Goto(gtNat2)) → False
instrConstrCheck(Write(wNat), Right) → False
instrConstrCheck(Write(wNat), Left) → False
instrConstrCheck(Write(wNat), Write(wNat2)) → True
instrConstrCheck(Write(wNat), Halt) → False
instrConstrCheck(Halt, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Halt, Goto(gtNat2)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(wNat2)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lookup(0', instrs) → instrs
instrsSecond(I(l, r)) → r
instrsFirst(I(l, r)) → l
getWrite(Write(int)) → int
getGotoSecond(IfGoto(i1, i2)) → i2
getGotoFirst(IfGoto(i1, i2)) → i1
getGoto(Goto(int)) → int
run(prog, tapeinput) → turing(prog, Nil, tapeinput, prog)
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
turing[Ite](True, I(IfGoto(i1, i2), r), revltape, rtape, prog) → turing(lookup(i2, prog), revltape, rtape, prog)
turing[Ite](False, I(l, r), revltape, rtape, prog) → turing(r, revltape, rtape, prog)

Types:
turing :: I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
I :: IfGoto:Goto:Right:Left:Write:Halt → I:Empty → I:Empty
IfGoto :: 0':S → 0':S → IfGoto:Goto:Right:Left:Write:Halt
Cons :: 0':S → Cons:Nil → Cons:Nil
turing[Ite] :: True:False → I:Empty → Cons:Nil → Cons:Nil → I:Empty → Cons:Nil
!EQ :: 0':S → 0':S → True:False
Goto :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
lookup :: 0':S → I:Empty → I:Empty
Right :: IfGoto:Goto:Right:Left:Write:Halt
Nil :: Cons:Nil
0' :: 0':S
Left :: IfGoto:Goto:Right:Left:Write:Halt
Write :: 0':S → IfGoto:Goto:Right:Left:Write:Halt
Halt :: IfGoto:Goto:Right:Left:Write:Halt
Empty :: I:Empty
S :: 0':S → 0':S
instrsConstrCheck :: I:Empty → I:Empty → True:False
True :: True:False
False :: True:False
instrConstrCheck :: IfGoto:Goto:Right:Left:Write:Halt → IfGoto:Goto:Right:Left:Write:Halt → True:False
notEmpty :: Cons:Nil → True:False
instrsSecond :: I:Empty → I:Empty
instrsFirst :: I:Empty → IfGoto:Goto:Right:Left:Write:Halt
getWrite :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoSecond :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGotoFirst :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
getGoto :: IfGoto:Goto:Right:Left:Write:Halt → 0':S
run :: I:Empty → Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_I:Empty2_0 :: I:Empty
hole_IfGoto:Goto:Right:Left:Write:Halt3_0 :: IfGoto:Goto:Right:Left:Write:Halt
hole_0':S4_0 :: 0':S
hole_True:False5_0 :: True:False
gen_Cons:Nil6_0 :: Nat → Cons:Nil
gen_I:Empty7_0 :: Nat → I:Empty
gen_0':S8_0 :: Nat → 0':S

Lemmas:
!EQ(gen_0':S8_0(n10_0), gen_0':S8_0(+(1, n10_0))) → False, rt ∈ Ω(0)

Generator Equations:
gen_Cons:Nil6_0(0) ⇔ Nil
gen_Cons:Nil6_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil6_0(x))
gen_I:Empty7_0(0) ⇔ Empty
gen_I:Empty7_0(+(x, 1)) ⇔ I(IfGoto(0', 0'), gen_I:Empty7_0(x))
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))

No more defined symbols left to analyse.

(21) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
!EQ(gen_0':S8_0(n10_0), gen_0':S8_0(+(1, n10_0))) → False, rt ∈ Ω(0)

(22) BOUNDS(1, INF)